es-update-iff(es;i;x;ds;e.P(e);s.f(s))
== (x:Id. vartype(i;x) r ds(x)?Top)
== c e@i.
== c (P(e)  ((x after e) = f((state when e)))) & ((P(e))  ((x after e) = (x when e))) 

latex

---

clarification:

es-update-iff(es;i;x;ds;e.P(e);s.f(s))
== (x:Id. es-vartype(es; i; x) r fpf-cap(ds;IdDeq;x;Top))
== c alle-at(es;i;e.(P(e)
== c alle-at(es;i;e.( (es-after(es; x; e) = f(es-state-when(es;e))  fpf-cap(ds;IdDeq;x;Top)))
== c & ((P(e))  (es-after(es; x; e) = es-when(es; x; e)  fpf-cap(ds;IdDeq;x;Top)))) 

latex

Definitions	A c B, x:A. B(x), Id, vartype(i;x), e@i. P(e), P & Q, (state when e), P  Q, A, f(x)?z, IdDeq, Top, (x after e), x when e
FDL editor aliases	es-update-iff